// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2018-2019 Ariadne Devos
/* sHT -- Spectre mitigations */

#ifndef _sHT_NOSPEC_H
#define _sHT_NOSPEC_H

/* See `doc/speculation.rst` for documentation */

#include <stddef.h>
#include <sys/types.h>
#include <limits.h>
#include <sHT/compiler.h>
#include <sHT/spectre.h>

/*@ ghost extern int speculation; */
/*@ axiomatic Speculation {
      predicate S{L1} = \at(speculation, L1) != 0;
      predicate NS{L1} = !S{L1};
    } */

/*@ terminates \true;
    assigns \nothing;
    behavior in_bounds:
      assumes pos < length;
      ensures \result == pos;
    behavior out_of_bounds:
      assumes pos >= length;
      requires S;
      ensures \result == 0;
    complete behaviors in_bounds, out_of_bounds;
    disjoint behaviors in_bounds, out_of_bounds; */
__attribute__((const))
static inline size_t
sHT_index_nospec(size_t pos, size_t length)
{

	/* Apparently invented locally.
	   Scratch registers: 0,
	   Instructions: ARM: 2 */
#if defined(_sHT_index_reduce)
	/*@ assigns pos \from pos, length;
	    ensures less: \old(pos) < length ==> pos == \old(pos);
	    ensures ge: \old(pos) >= length ==> pos == 0; */
	_sHT_index_reduce(&pos, length);
	return pos;

	/* Invented by (???? see Linux archives)
	   Scratch registers: 1
	   Instructions: ARM, X86: 3
	   See <https://lwn.net/Articles/744287/> */
#elif defined(_sHT_index_mask)
	size_t mask;
	/*@ assigns mask \from pos, length;
	    ensures mask_s: \initialized(&mask);
	    ensures less: pos < length ==> mask == SIZE_MAX;
	    ensures ge: pos >= length ==> mask == 0; */
	_sHT_index_mask(&mask, pos, length);
	return pos & mask;
#else
#  error Define speculative index correction for your architecture!
#endif
}

#if 0
/* Note to the future: you can't cheat GCC's
  'no output operands for asm goto' restriction. */
static inline _Bool
sHT_index_test_nospec(size_t *i, size_t length)
{
	sHT_hide_var(*i);
	/* Modify `i` behind GCC's back */
	_sHT_index_test_mask(i, length, out_of_bounds);
	sHT_hide_var(*i);
	return 1;

out_of_bounds:
	sHT_hide_var(*i);
	return 0;
}
#endif

/** Stop the current execution if the processor is speculating incorrectly

  TODO: convince researchers and the industry to stop speculating,
  at least limiting theirselves to control-flow speculation (which is
  rather controllable, compared to other forms of speculation). Each
  additional side-channel makes security harder. */
/*@ requires \true;
    terminates \true;
    assigns \nothing;
    ensures S{Pre} ==> \false; */
static void
sHT_despeculate()
{
	/* volatile "memory" is for paranoia, to avoid reordering or
	  or elimination (Linux does this -- volatility, and GCC documentation
	  allows that -- reordering and elimination). Although in my tests
	  (GCC 6.3.0, GCC 8.3.0, Clang 6.0), even without any of these nothing
	  happens. */
	/*@ requires \true;
	    assigns \nothing;
	    ensures S{Pre} ==> \false; */
	_sHT_speculation_barrier();
}

#endif
